<html><head><style type="text/css">body{font-family:Arial,Helvetica,sans-serif;text-align:center;background:#ffffff}td.colhead{font-weight:bold;text-align:center;background:#ffffff}td.rowhead{font-weight:bold;background:#ffffff}td.cell{text-align:center;padding:5px,0}tr.even{background:#a0a0d0}tr.odd{background:#c0c0f0}td.empty{background:#ffffff}</style><html>
  <head>
    <style type="text/css">
      <!--
        tr.even { background-repeat: repeat; background-color: #a0a0d0; background-attachment: scroll }
        td.empty { background-repeat: repeat; background-color: #ffffff; background-attachment: scroll }
        body { background-repeat: repeat; background-color: #ffffff; font-family: Arial,Helvetica,sans-serif; background-attachment: scroll; text-align: center }
        tr.odd { background-repeat: repeat; background-color: #c0c0f0; background-attachment: scroll }
        td.rowhead { background-repeat: repeat; font-weight: bold; background-color: #ffffff; background-attachment: scroll }
        td.colhead { background-repeat: repeat; font-weight: bold; background-color: #ffffff; background-attachment: scroll; text-align: center }
        td.cell { padding-right: 0; text-align: center; padding-left: 0; padding-bottom: 0; padding-top: 0 }
      -->
    </style>
    
  </head>
  <body>
    <h2>
      Petri net invariant analysis results
    </h2>
    <h3>
      T-Invariants
    </h3>
    <table border="0" cellspacing="2">
      <tr class="odd">
        <td class="colhead">
          Norte
        </td>
        <td class="colhead">
          Sur
        </td>
        <td class="colhead">
          Este
        </td>
        <td class="colhead">
          Oeste
        </td>
        <td class="colhead">
          Disparar-N
        </td>
        <td class="colhead">
          Disparar-S
        </td>
        <td class="colhead">
          Disparar-E
        </td>
        <td class="colhead">
          Disparar-O
        </td>
        <td class="colhead">
          PasarE-N
        </td>
        <td class="colhead">
          PasarO-S
        </td>
        <td class="colhead">
          PasarS-E
        </td>
        <td class="colhead">
          PasarN-O
        </td>
        <td class="colhead">
          Restart-N
        </td>
        <td class="colhead">
          Restart-S
        </td>
        <td class="colhead">
          Restart-E
        </td>
        <td class="colhead">
          Restart-O
        </td>
      </tr>
      <tr class="even">
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
      </tr>
      <tr class="odd">
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
      </tr>
      <tr class="even">
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
      </tr>
      <tr class="odd">
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
      </tr>
      <tr class="even">
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
      </tr>
      <tr class="odd">
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
      </tr>
      <tr class="even">
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
      </tr>
      <tr class="odd">
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
      </tr>
      <tr class="even">
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
      </tr>
      <tr class="odd">
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
      </tr>
      <tr class="even">
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
      </tr>
      <tr class="odd">
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          0
        </td>
        <td class="cell">
          1
        </td>
      </tr>
    </table>
    The net is covered by positive T-Invariants, therefore it might be bounded 
    and live.<br><br>

    <h3>
      P-Invariants
    </h3>
    <table border="0" cellspacing="2">
      <tr class="odd">
        <td class="colhead">
          Radar
        </td>
        <td class="colhead">
          Enem-N
        </td>
        <td class="colhead">
          Enem-S
        </td>
        <td class="colhead">
          Enem-E
        </td>
        <td class="colhead">
          Enem-O
        </td>
        <td class="colhead">
          Destruido-N
        </td>
        <td class="colhead">
          Destruido-S
        </td>
        <td class="colhead">
          Destruido-E
        </td>
        <td class="colhead">
          Destruido-O
        </td>
      </tr>
      <tr class="even">
        <td class="cell">
          1
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          1
        </td>
        <td class="cell">
          1
        </td>
      </tr>
    </table>
    The net is covered by positive P-Invariants, therefore it is bounded.<br>

    <h3>
      P-Invariant equations
    </h3>
    M(Radar) + M(Enem-N) + M(Enem-S) + M(Enem-E) + M(Enem-O) + M(Destruido-N) 
    + M(Destruido-S) + M(Destruido-E) + M(Destruido-O) = 4<br><br><br>Analysis 
    time: 0.02s
  </body>
</html>
